Nuprl Definition : es-interval 0,22

[e, e'] == filter(ev.es-ble{i:l}(es;e;ev);before(e') @ [e']) 
latex



clarification:

es-interval{i:l}(es; e; e') == filter(ev.es-ble{i:l}(es; e; ev);es-before(es; e') @ (e'.nil)) 
latex


Definitions[e, e'], filter(P;l), es-ble{i:l}(es;e;e'), as @ bs, before(e)
FDL editor aliaseses-interval

origin